T:Type, P:(T), L, L':(T List). (xL. P(x))  (L = L')  (L = L'  ({x:T| P(x)}  List)) 

latex

Definitions	xL. P(x), x(s), Type, S  T, type List, , A  B, A, False, s = t, , a < b, x:AB(x), {x:A| B(x)} , , x:A. B(x), x. t(x), P  Q, x.A(x), f(a), t  T, ||as||, <a, b>, l[i], Void, #$n, (x  l), {i..j}, i  j < k, P & Q, x:A  B(x)
Lemmas	le wf, select member, select wf, list-set-type2, nat wf, length wf1, list extensionality, l all wf